T:Type, g:Top, L:(T List), f:({x:T| (x  L)} (Top + Top)).
concat(map(x.map(y.g(x,y);case f(x) of inl(m) => [m] | inr(x) => []);L))
~
mapfilter(x.g(x,outl(f(x)));x.isl(f(x));L) 

latex

Definitions	t  T, reduce(f;k;as), Y, filter(P;l), mapfilter(f;P;L), map(f;as), concat(ll), x:A. B(x), as @ bs, True, b, P  Q, , ff, tt, i <z j, b, i z j, nth_tl(n;as), hd(l), P & Q, i  j < k, ||as||, {i..j}, l[i], if b then t else f fi , isl(x), outl(x), x(s), A, False, P  Q, Unit, ,
Lemmas	top wf, l member wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, false wf, true wf, eqtt to assert, bool wf, non neg length, length wf1, select member, isl wf